﻿// Spun AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Formality.Levels;
using Formality.Logic.Game;
using Formality.FormalSystem;

namespace Formality.Game
{
    public class ProofChecker
    {
        public ProofChecker(string Name, bool Trace)
        {
            this.ShowTrace = Trace;
            this.Name = Name;
            BadProofs = new List<string>();

            Problems = (from P in new FullEnumerator()
                        select new Problem
                        {
                            Id = P.Id,
                            Goal = Sentence.Parse(P.ToString())
                        }).ToList();
        }

        public IEnumerable<string> Failures { get { return BadProofs; } }

        public bool Check()
        {
            var Player = new Player(Name);

            foreach (var Problem in Problems)
            {
                Trace("----------------------");
                Trace("Checking " + Problem.Id + " " + Problem.Goal);
                Trace("----------------------");

                var Submissions = Player.ProblemSubmissions(Problem.Id).ToArray();

                if (Submissions.Length > 0)
                {
                    if (!Check(Submissions, Problem))
                        BadProofs.Add(Problem.Id);
                }
            }

            return BadProofs.Count == 0;
        }

        private bool Check(string[] Submissions, Problem Problem)
        {
            var Premises = new List<Sentence>(GetPremises(Problem.Id));

            foreach (var Submission in Submissions)
            {
                Proposition Proposition;

                try
                {
                    var Parsed = Sentence.Parse(Submission);
                    Proposition = (Proposition)Parsed;
                }
                catch (Exception)
                {
                    Trace("Could not find a proposition: " + Submission);
                    continue;
                }

                if (CanInfer(Proposition, Premises))
                {
                    if (Proposition.Equals(Problem.Goal))
                    {
                        Trace("Can infer the goal: " + Proposition);
                        return true;
                    }
                    else
                    {
                        Trace(Proposition);
                        Premises.Add(Proposition);
                    }
                }
                else
                {
                    Trace("Cannot infer " + Proposition);
                }
            }

            return false;
        }

        private void Trace(object o)
        {
            if (ShowTrace)
                Console.WriteLine(o);
        }

        private bool CanInfer(Proposition Parsed, List<Sentence> Premises)
        {
            foreach (var Premise in Premises)
                if (Premise.Implies(Parsed, Premises).HasValue)
                    return true;
            return false;
        }

        private IEnumerable<string> AllProblemIds
        {
            get { return from S in Problems select S.Id; }
        }

        private Sentence GetProblem(string Id)
        {
            return (from P in Problems where P.Id == Id select P.Goal).Single();
        }

        private IEnumerable<Sentence> GetPremises(string Id)
        {
            return Problems
                .TakeWhile(P => P.Id != Id)
                .Select(P => P.Goal);
        }

        private bool ShowTrace;
        private string Name;
        private List<string> BadProofs;
        private List<Problem> Problems;

        private class Problem
        {
            public string Id;
            public Sentence Goal;
        }
    }
}
